Termination Proof Script

• Consider the SCC {7}. There are no usable rules. By taking the AF π with π(MIN) = 1 together with the lexicographic path order with empty precedence, rule 7 is strictly decreasing.


• Consider the SCC {8}. The usable rules are {1,2}. By taking the AF π with π(min) = π(QUOT) = 1 together with the lexicographic path order with empty precedence, rule 1 is weakly decreasing and the rules in {2,8} are strictly decreasing.


• Consider the SCC {10}. The usable rules are {1-4}. By taking the AF π with π(LOG) = π(min) = π(quot) = 1 together with the lexicographic path order with empty precedence, the rules in {1,3,4} are weakly decreasing and the rules in {2,10} are strictly decreasing.